package base;

import java.util.ArrayList;

import resolution.Resolution;

/**
 * Created by IntelliJ IDEA. User: njussien Date: 30/11/12 Time: 10:37
 */
public class Ou extends OperateurBinaire {

	// ///////////////
	// CONSTRUCTOR //
	// ///////////////

	public Ou(Formule a, Formule b) {
		super(a, b);
	}

	// ///////////
	// METHODS //
	// ///////////

	@Override
	public Formule negation() {
		return new Et(operande.negation(), operandedroit.negation());
	}

	@Override
	public Formule descendreNon() {
		return new Ou(operande.descendreNon(), operandedroit.descendreNon());
	}

	public String toString() {
		return "[Operande:(" + operande.toString() + " OU " + operandedroit.toString() + ")] ";
	}

	@Override
	public Formule enleveEquImp() {
		return new Ou(operande.enleveEquImp(), operandedroit.enleveEquImp());
	}

	public void renommer() {
		Formule f = operande;
		int nbChang = 0;

		// on renomme chaque variable des pour tout
		while (f instanceof Quantification) {
			if (f instanceof PourTout) {
				Variable aSubstituer = new Variable(((PourTout) f).getX().nom + nbChang);
				nbChang++;
				Formule f2 = operande;
				while (f2 instanceof Quantification) {
					// on substitue la nouvelle variable a l ancienne
					if (((Quantification) f2).getX().equals(((PourTout) f).getX())) {
						Variable avant = ((Quantification) f2).getX();
						((Quantification) f2).setX(aSubstituer);
						((Quantification) f2).substituer(avant, aSubstituer);
					}
				}
			}
			f = ((Quantification) f).getF();
		}

		f = operandedroit;

		while (f instanceof Quantification) {
			if (f instanceof PourTout) {
				Variable aSubstituer = new Variable(((PourTout) f).getX().nom + nbChang);
				nbChang++;
				Formule f2 = operandedroit;
				while (f2 instanceof Quantification) {
					if (((Quantification) f2).getX().equals(((PourTout) f).getX())) {
						Variable avant = ((Quantification) f2).getX();
						((Quantification) f2).setX(aSubstituer);
						((Quantification) f2).substituer(avant, aSubstituer);
					}
				}
			}
			f = ((Quantification) f).getF();
		}
		operande.renommer();
		operandedroit.renommer();
	}

	@Override
	public Formule remonterQuantificateurs() {

		operande = operande.remonterQuantificateurs();
		operandedroit = operandedroit.remonterQuantificateurs();

		Formule f = operande;
		while (f instanceof Quantification) {
			if (f instanceof PourTout) {
				Formule f2 = operandedroit;
				while (f2 instanceof Quantification) {
					if (((Quantification) f2).getX().getName().equals(((PourTout) f).getX().getName())) {
						operande.substituer(new Variable("varRemont" + Resolution.CHANGEMENT_RENOMMAGE_REMONTER_QUANTIF++), ((Existe) f).getX());
						break;
					}
					f2 = ((Quantification) f2).getF();
				}
			}
			f = ((Quantification) f).getF();

		}
		if (operande instanceof Quantification) {
			if (operande instanceof Existe) {
				Formule fdroit = null;
				Formule fdroitPrecedant = operandedroit;
				while (fdroit instanceof Quantification) {
					if (((Quantification) fdroit).x.getName().equals(((Quantification) operande).x.getName())) {
						// on est assure par l'avance que l'on est dans le bon
						// cas
						if (fdroit == null) {
							operandedroit = ((Quantification) fdroit).getF();
						} else {
							((Quantification) fdroitPrecedant).setF(((Quantification) fdroit).getF());
						}
						break;
					} else {
						fdroitPrecedant = fdroit;
						fdroit = ((Quantification) fdroit).getF();
					}
				}
				return new Existe(((Quantification) operande).x, new Ou(((Quantification) operande).getF().remonterQuantificateurs(), operande.remonterQuantificateurs()));
			} else {
				return new PourTout(((Quantification) operande).x, new Ou(((Quantification) operande).getF().remonterQuantificateurs(), operande.remonterQuantificateurs()));
			}
		} else if (operandedroit instanceof Quantification) {
			if (operandedroit instanceof Existe) {
				Formule fdroit = null;
				Formule fdroitPrecedant = operande;
				while (fdroit instanceof Quantification) {
					if (((Quantification) fdroit).x.getName().equals(((Quantification) operandedroit).x.getName())) {
						// on est assure par l'avance que l'on est dans le bon
						// cas
						if (fdroit == null) {
							operande = ((Quantification) fdroit).getF();
						} else {
							((Quantification) fdroitPrecedant).setF(((Quantification) fdroit).getF());
						}
						break;
					} else {
						fdroitPrecedant = fdroit;
						fdroit = ((Quantification) fdroit).getF();
					}
				}

				return new Existe(((Quantification) operandedroit).x, new Ou(((Quantification) operande).getF().remonterQuantificateurs(), operande.remonterQuantificateurs()));
			} else {
				return new PourTout(((Quantification) operandedroit).x, new Ou(((Quantification) operande).getF().remonterQuantificateurs(), operande.remonterQuantificateurs()));
			}
		} else {
			return this;
		}
	}

	@Override
	public Formule toConjonctive() {

		operande = operande.toConjonctive();
		operandedroit = operandedroit.toConjonctive();

		if (operande instanceof Et) {
			return new Et(new Ou(((Et) operande).getOperande(), operandedroit).toConjonctive(), new Ou(((Et) operande).getOperandedroit(), operandedroit).toConjonctive());
		}

		if (operandedroit instanceof Et) {
			return new Et(new Ou(((Et) operandedroit).getOperande(), operande).toConjonctive(), new Ou(((Et) operandedroit).getOperandedroit(), operande).toConjonctive());
		}

		return this;

	}

	public Formule supprimer(Atome a) {
		if (operande instanceof Atome && ((Atome) operande).equals(a)) {
			// si on veut supprimer A() et que F = A ou A : F =vide
			if (operandedroit instanceof Atome && ((Atome) operandedroit).equals(a)) {
				return null;
			} else {
				return operandedroit;
			}
		} else if (operandedroit instanceof Atome && ((Atome) operandedroit).equals(a)) {
			// si on veut supprimer A() et que F = A ou A : F =vide
			if (operande instanceof Atome && ((Atome) operande).equals(a)) {
				return null;
			} else {
				return operande;
			}
		} else {
			return new Ou(operande instanceof Ou ? ((Ou) operande).supprimer(a) : operande, operandedroit instanceof Ou ? ((Ou) operandedroit).supprimer(a) : operandedroit);
		}
	}

	public Formule supprimer(Non a) {
		if (operande instanceof Non && ((Non) operande).equals(a)) {
			// si on veut supprimer A() et que F = A ou A : F =vide
			if (operandedroit instanceof Non && ((Non) operandedroit).equals(a)) {
				return null;
			} else {
				return operandedroit;
			}
		} else if (operandedroit instanceof Non && ((Non) operandedroit).equals(a)) {
			// si on veut supprimer A() et que F = A ou A : F =vide
			if (operande instanceof Non && ((Non) operande).equals(a)) {
				return null;
			} else {
				return operande;
			}
		} else {
			return new Ou(operande instanceof Ou ? ((Ou) operande).supprimer(a) : operande, operandedroit instanceof Ou ? ((Ou) operandedroit).supprimer(a) : operandedroit);
		}
	}

	public ArrayList<Formule> reccupererAllAtomeNon() {
		ArrayList<Formule> ret = new ArrayList<Formule>();

		if (operande instanceof Atome)
			ret.addAll(((Atome) operande).reccupererAllAtomeNon());
		else if (operande instanceof Non) {
			ret.addAll(((Non) operande).reccupererAllAtomeNon());
		} else {
			ret.addAll(((Ou) operande).reccupererAllAtomeNon());
		}

		if (operandedroit instanceof Atome)
			ret.addAll(((Atome) operandedroit).reccupererAllAtomeNon());
		else if (operandedroit instanceof Non) {
			ret.addAll(((Non) operandedroit).reccupererAllAtomeNon());
		} else {
			ret.addAll(((Ou) operandedroit).reccupererAllAtomeNon());
		}

		return ret;
	}

	@Override
	public Formule copy() {
		return new Ou(operande.copy(), operandedroit.copy());
	}
}
